Nuprl Definition : R-pre-init1
0,22
postcript
pdf
R-pre-init1(
i
;
x
;
A
;
x0
;
a
;
T
;
P
) == R-pre-init(
i
;
x
:
A
;
x
:
x0
;
a
;
T
;
s
,
v
.
P
(
s
(
x
),
v
))
latex
Definitions
R-pre-init(
i
;
ds
;
init
;
a
;
T
;
P
)
,
x
:
v
,
x
.
A
(
x
)
,
f
(
a
)
FDL editor aliases
R-pre-init1
origin
s,v. P(s(x),v)) s,v. P(s(x),v)) x.A(x)